Monadic predicate calculus

In logic, the monadic predicate calculus is the fragment of predicate calculus in which all predicate letters are monadic (that is, they take only one argument), and there are no function letters. All atomic formulae have the form , where is a predicate letter and is a variable.

Monadic predicate logic can be contrasted with polyadic predicate logic, which uses predicates (called many-place predicates) that take two or more arguments. For example, "x is mortal" or "Mx" is a one-place predicate, while "x loves y" or "Lxy" is a two-place predicate and "x lies between y and z" or "Bxyz" is a three-place predicate.^[1]

The absence of polyadic predicates severely restricts what can be expressed in the monadic predicate calculus. That calculus is so weak that, unlike the full predicate calculus, it is decidable whether a given formula of that calculus is logically valid (true for all nonempty domains).^[2][3] (However, adding a single binary predicate letter to monadic logic would result in a system with the expressive power of the full predicate calculus.) Because the monadic predicate calculus is decidable, it is ipso facto inadequate for general mathematical reasoning, if only because the tiny fragment of mathematics called Peano arithmetic is known to be undecidable.

Notwithstanding the above deficiencies, the need to go beyond monadic logic was not appreciated until the work on the logic of relations, by Augustus DeMorgan and Charles Sanders Peirce in the 19th century, and by Frege in his little-read 1879 Begriffsschrifft. Prior to the work of these three men, syllogistic term logic was widely considered adequate for formal deductive reasoning.

Inferences in term logic can all be represented in the monadic predicate calculus. For example the syllogism

All dogs are mammals

No mammal is a herbivore

Thus, no dog is a herbivore

can be notated in the language of monadic predicate calculus as

where , and denote the predicates of being, respectively, a dog, a mammal, and a herbivore.

Conversely, monadic predicate calculus is not significantly more expressive than term logic. It is easily proved that every formula in the monadic predicate calculus is equivalent to a formula in which quantifiers appear only in closed subformulae of the form

or

Each of these formulas is the negation of the other, and the quantifiers do not nest. These formulas also generalize slightly the form of basic judgements considered in term logic. For example, this form allows statements such as "Every mammal is either a herbivore or a carnivore (or both)", . Reasoning about such statements can, however, still be handled within the framework of term logic, although not by the 19 classical Aristotelian syllogisms alone.

Taking propositional logic as given, every formula in the monadic predicate calculus expresses something that can likewise be formulated in term logic. On the other hand, a modern view of the problem of multiple generality in traditional logic concludes that quantifiers cannot nest usefully if there are no polyadic predicates to relate the bound variables.

Variants

The formal system describe in this entry is sometimes called the pure monadic predicate calculus, where "pure" signifies the absence of function letters. Allowing monadic function letters changes the logic only superficially, whereas admitting even a single binary function letter would result in a system with the expressive power of the full predicate calculus.

Monadic predicate calculus is also called monadic first-order logic. Monadic second-order logic keeps the requirement that all predicates be unary, but allows for quantification over predicates as well as variables.

Footnotes

1. ^ http://www.earlham.edu/~peters/courses/log/terms3.htm
2. ^ Heinrich Behmann, Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem, in Mathematische Annalen (1922)
3. ^ Löwenheim, L. (1915) "Über Möglichkeiten im Relativkalkül," Mathematische Annalen 76: 447-470. Translated as "On possibilities in the calculus of relatives" in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press: 228-51.

Logic   Overview Academic areas Argumentation theory Axiology Critical thinking Computability theory Formal semantics History of logic Informal logic Logic in computer science Mathematical logic Mathematics Metalogic Metamathematics Model theory Philosophical logic Philosophy Philosophy of logic Philosophy of mathematics Proof theory Set theory Foundational concepts Abduction Analytic truth Antinomy A priori Deduction Definition Description Entailment Induction Inference Logical consequence Logical form Logical implication Logical truth Name Necessity Meaning Paradox Possible world Presupposition Probability Reason Reasoning Reference Semantics Statement Strict implication Substitution Syntax Truth Truth value Validity   Philosophical logic Critical thinking and Informal logic Analysis Ambiguity Argument Belief Bias Credibility Evidence Explanation Explanatory power Fact Fallacy Inquiry Opinion Parsimony Premise Propaganda Prudence Reasoning Relevance Rhetoric Rigor Vagueness Theories of deduction Constructivism Dialetheism Fictionalism Finitism Formalism Intuitionism Logical atomism Logicism Nominalism Platonic realism Pragmatism Realism   Metalogic and metamathematics Cantor's theorem Church's theorem Church's thesis Consistency Effective method Foundations of mathematics Gödel's completeness theorem Gödel's incompleteness theorems Soundness Completeness Decidability Interpretation Löwenheim–Skolem theorem Metatheorem Satisfiability Independence Type–token distinction Use–mention distinction   Mathematical logic General Formal language Formation rule Formal system Deductive system Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Natural deduction Rule of inference Relation Theorem Logical consequence Axiomatic system Type theory Symbol Syntax Theory Traditional logic Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram Propositional calculus and Boolean logic Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables Predicate First-order Quantifiers Predicate Second-order Monadic predicate calculus Set theory Set Empty set Enumeration Extensionality Finite set Function Subset Power set Countable set Recursive set Domain Range Ordered pair Uncountable set Model theory Model Interpretation Non-standard model Finite model theory Truth value Validity Proof theory Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax Computability theory Recursion Recursive set Recursively enumerable set Decision problem Church–Turing thesis Computable function Primitive recursive function   Non-classical logic Modal logic Alethic Axiologic Deontic Doxastic Epistemic Temporal Intuitionism Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory Fuzzy logic Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations Substructural logic Structural rule Relevance logic Linear logic Paraconsistent logic Dialetheism Description logic Ontology Ontology language   Logicians Anderson Aristotle Averroes Avicenna Bain Barwise Bernays Boole Boolos Cantor Carnap Church Chrysippus Curry De Morgan Frege Geach Gentzen Gödel Hilbert Kleene Kripke Leibniz Löwenheim Peano Peirce Putnam Quine Russell Schröder Scotus Skolem Smullyan Tarski Turing Whitehead William of Ockham Wittgenstein Zermelo   Lists Topics Outline of logic Index of logic articles Mathematical logic Boolean algebra Set theory Other Logicians Rules of inference Paradoxes Fallacies Logic symbols Portal Category Outline WikiProject Talk changes